import Mathlib

namespace CNVSTargetAttackBound

/--
Modello di target probabilistico CNVS.

`pcomp` = probabilità di compromissione del singolo frammento critico.
`m` = numero di frammenti critici.
`eta` = probabilità massima di attacco tollerata.
-/
structure TargetModel where
  pcomp : ℝ
  m : Nat
  eta : ℝ

  hpcomp_nonneg : 0 ≤ pcomp
  hpcomp_lt_one : pcomp < 1
  heta_pos : 0 < eta
  heta_lt_one : eta < 1

/--
Bound di attacco secondo il Teorema 17a:

P(Rec*) ≤ pcomp^m.
-/
noncomputable def AttackBound (M : TargetModel) : ℝ :=
  M.pcomp ^ M.m

/--
Il target è soddisfatto se il bound teorico è sotto η.
-/
def TargetSatisfied (M : TargetModel) : Prop :=
  AttackBound M ≤ M.eta

/--
Se pcomp^m ≤ η, allora il target di sicurezza è soddisfatto.
-/
theorem target_satisfied_if_power_bound
    (M : TargetModel)
    (h : M.pcomp ^ M.m ≤ M.eta) :
    TargetSatisfied M := by
  exact h

/--
Se il target è soddisfatto, allora il bound teorico
garantisce P(Rec*) ≤ η, assumendo P(Rec*) ≤ AttackBound.
-/
theorem probability_below_target
    (M : TargetModel)
    (PRec : ℝ)
    (hProb : PRec ≤ AttackBound M)
    (hTarget : TargetSatisfied M) :
    PRec ≤ M.eta := by
  exact le_trans hProb hTarget

/--
Esempio positivo:
pcomp = 1/2
m = 4
eta = 1/10

(1/2)^4 = 1/16 ≤ 1/10
-/
noncomputable def PositiveTargetExample : TargetModel where
  pcomp := 1 / 2
  m := 4
  eta := 1 / 10

  hpcomp_nonneg := by norm_num
  hpcomp_lt_one := by norm_num
  heta_pos := by norm_num
  heta_lt_one := by norm_num

example :
    AttackBound PositiveTargetExample = 1 / 16 := by
  norm_num [AttackBound, PositiveTargetExample]

example :
    TargetSatisfied PositiveTargetExample := by
  unfold TargetSatisfied AttackBound PositiveTargetExample
  norm_num

/--
Esempio negativo:
pcomp = 1/2
m = 2
eta = 1/10

(1/2)^2 = 1/4 > 1/10
-/
noncomputable def NegativeTargetExample : TargetModel where
  pcomp := 1 / 2
  m := 2
  eta := 1 / 10

  hpcomp_nonneg := by norm_num
  hpcomp_lt_one := by norm_num
  heta_pos := by norm_num
  heta_lt_one := by norm_num

example :
    AttackBound NegativeTargetExample = 1 / 4 := by
  norm_num [AttackBound, NegativeTargetExample]

example :
    ¬ TargetSatisfied NegativeTargetExample := by
  unfold TargetSatisfied AttackBound NegativeTargetExample
  norm_num

end CNVSTargetAttackBound